Nuprl Lemma : mon_nat_op_add
13,42
postcript
pdf
g
:IMonoid,
e
:|
g
|,
a
,
b
:
. ((
a
+
b
)
e
) = ((
a
e
) * (
b
e
))
|
g
|
latex
Up
groups
1
Definitions of Statement
n
e
Definitions
n
e
Lemmas
nat
op
add
origin
g:IMonoid, e:|g|, a, b:
. ((a+b) 
e) = ((a e) * (b e)) 
|g| g:IMonoid, e:|g|, a, b:. ((a+b) e) = ((a e) * (b e)) |g| e e